Issue4390irrelevance.agda:10,29-30
(.A → A) !=< (A → A) because one is a relevant function type and
the other is an irrelevant function type
when checking that the expression f has type A → A
